Nuprl Lemma : gcd_p_eq_args 2,24

a:. GCD(a;a;a
latex


DefinitionsGCD(a;b;y), P  Q, P & Q, Prop, b | a, x:AB(x), t  T
Lemmasdivides reflexivity, divides wf

origin